Definitions | False, P  Q, A, t T, x:A. B(x), b,  b, , s = t, prop{i:l}, Knd, Type, x.A(x),  x. t(x), top, fpf(A; a.B(a)), x:A B(x), Kind-deq, fpf-dom(eq; x; f), x:A B(x), P Q, P   Q, Unit, left + right, fpf-ap(f; eq; x), normal-type{i:l}(T), void, if b then t else f fi , fpf-all(A; eq; f; x,v.P(x;v)), fpf-cap(f; eq; x; z), normal-da{i:l}(da) |